Inference at * 
Iof proof for Lemma bfalse wf:


  ff   

latex

 by ((Unfolds ``bfalse bool`` 0) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n
C),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C.

Definitions	ff, , t  T
Lemmas	unit wf, it wf